Nuprl Definition : rv-disjoint 11,40

rv-disjoint(p;n;X;Y)
== i:{0..n}.
== (s1s2:({0..n}Outcome). (j:{0..n}. ((j = i))  (s1(j) = s2(j)))  (X(s1) = X(s2)))
==  (s1s2:({0..n}Outcome).
==  (j:{0..n}. ((j = i))  (s1(j) = s2(j)))  (Y(s1) = Y(s2))) 
latex



clarification:

rv-disjoint(p;n;X;Y)
== i:{0..n}.
== (s1:({0..n}p-outcome(p)), s2:({0..n}p-outcome(p)).
== (j:{0..n}. ((j = i  ))  (s1(j) = s2(j p-outcome(p)))  (X(s1) = X(s2 ))
==  (s1:({0..n}p-outcome(p)), s2:({0..n}p-outcome(p)).
==  (j:{0..n}. ((j = i  ))  (s1(j) = s2(j p-outcome(p)))  (Y(s1) = Y(s2 )) 
latex


DefinitionsP  Q, x:AB(x), x:AB(x), {i..j}, #$n, P  Q, A, , Outcome, s = t, , f(a)
FDL editor aliasesrv-disjoint

origin